|
===================================== 〔語彙分解〕的な部分一致の検索結果は以下の通りです。 ・ 正 ： [ただし, せい, しょう] 【名詞】 1. (logical) true 2. regular ・ 正当 ： [せいとう] 1. (adj-na,n) just 2. justifiable 3. right 4. due 5. proper 6. equitable 7. reasonable 8. legitimate 9. lawful ・ 正当性 ： [せいとうせい] 【名詞】 1. legal 2. proper ・ 計 ： [けい] 1. (n,n-suf) plan ・ 計算 ： [けいさん] 1. (n,vs) (1) calculation 2. reckoning 3. count 4. (2) forecast ・ 計算機 ： [けいさんき] 【名詞】 1. computer 2. calculator ・ 機 ： [き, はた] (n) loom ・ 科 ： [か] 1. (n,n-suf) department 2. section ・ 科学 ： [かがく] 【名詞】 1. science ・ 学 ： [がく] 【名詞】 1. learning 2. scholarship 3. erudition 4. knowledge
計算機科学における正当性（Correctness）とは、アルゴリズムがその仕様に照らして正しいことを意味する。「機能的」正当性とは、アルゴリズムの入出力動作に関する正当性である（すなわち、各入力に対して正しく出力を生成すること）。形式的検証を参照されたい。 完全正当性（Total Correctness）は、アルゴリズムが常に停止することも要求される。一方、部分正当性（Partial Correctness）は単に返ってくる答えが正しいことのみを要求する（常に答えが返ってくるとは限らない）。停止問題には汎用的解法はないので、完全正当性はより深い問題をはらんでいる。 例えば、整数を 1 から順に調べて奇数の完全数を探すとした場合、部分正当性を備えたプログラムを書くのは極めて簡単である（素因数分解を行って ''n'' が完全数かどうかを調べる）。しかし、そのプログラムが完全正当性を備えているとするには数論において未知の知識を必要とする。 正当性の証明は数学的証明でなければならず、アルゴリズムもその仕様記述も形式的に与えられなければならない（形式的仕様記述）。特にその証明は、そのアルゴリズムを特定のマシン上でプログラムとして実装したものについて正当性を意味するものではない。その場合メモリ量の限界を考慮する必要がある。 証明論におけるカリー・ハワード対応は、直観主義論理における機能的正当性の証明がラムダ計算における特定プログラムに対応するとしている。このような証明の変換を「プログラム抽出; program extraction」と呼ぶ。 ==関連項目== *ホーア論理 *形式的検証 *契約プログラミング 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「正当性 (計算機科学)」の詳細全文を読む スポンサード リンク
|